Nuprl Definition : w-E
0,22
postcript
pdf
E == {
p
:(Id
)|
isnull(a(1of(
p
);2of(
p
))) }
latex
clarification:
w-E(
w
) == {
p
:(Id
)|
w-isnull(
w
; w-a(
w
; 1of(
p
); 2of(
p
))) }
latex
Definitions
E
,
Id
,
,
A
,
b
,
isnull(
a
)
,
a(
i
;
t
)
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
w-E
origin
)| 
isnull(a(1of(p);2of(p))) }
)| w-isnull(w; w-a(w; 1of(p); 2of(p))) } )| isnull(a(1of(p);2of(p))) }
)| w-isnull(w; w-a(w; 1of(p); 2of(p))) } A
b